A:Type, P:(A), L:A List. ||filter(P;L)|| = count(P;L)   

latex

Definitions	, t  T, x:A. B(x), count(P;L), filter(P;l), ||as||, reduce(f;k;as), AB, True, T, b, A, b, Prop, , P  Q, P & Q, P  Q, Unit, if b t else f fi, False
Lemmas	le wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, assert wf, length wf1, filter wf, count wf, nat wf